/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2004  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: BddNodePool.java,v 1.6 2004/03/15 02:07:01 fqian Exp $
package SableJBDD.bdd.internal;

import SableJBDD.bdd.*;
import java.io.PrintStream;
import java.lang.ref.*;
import java.lang.reflect.*;

/**
 * A BDD node pool pre-allocates and recycles bdd nodes. This class implements
 * all necessary pooling functions, including adding, creating nodes. When
 * the pool is empty, new nodes are created and subclasses
 * get notified of newNodeCreated event, and can perform some pooling and
 * recycling operations by changing pooled node queue.
 *
 * @author Feng Qian
 */
public abstract class BddNodePool implements BddNodeFactory{

  // pool head node
  protected JBddNode head, tail;
  
  // each node is hold by a phantom reference
  private int numberOfAllocations = 0;
  private int preAllocatedNodes   = 0;
  
  /**
   * Defines a pool with an initial number of pre-allocated nodes.
   */
  protected BddNodePool(int size) {
    this.tail = new JBddInternalNode(null);
    this.head = this.tail;
    for (int i=1; i<size; i++) {
      this.head = new JBddInternalNode(this.head);
    }
    this.preAllocatedNodes = size;
  }
 
  protected boolean empty() {
    return this.head == null;
  }

  protected synchronized void add(JBddNode node) {
    // node must node had the next
    // assert node.getNext() == null;

    if (this.tail == null) {
      this.head = this.tail = node;
    } else {
      this.tail.setNext(node);
      this.tail = node;
    }
  }
  
  protected synchronized JBddNode removeFirst() {
    // assert this.head != null;
    JBddNode node = this.head;
    this.head = this.head.getNext();
    node.clearNext();
    if (this.head == null) this.tail = null;
    return node;
  }
 
  // subclass got this event
  protected abstract void newNodeCreated(JBddNode node);
  
  /**
   * Gets a node from a pool either by reusing an existing node
   * or by creating a new object.
   * NOTE: a JBddNode is a unique object, 
   */
  public JBddNode getFreshNode(JBddVariable var, 
                               JBddNode low, 
                               JBddNode high) {
    if (empty()){
      this.numberOfAllocations++;
      JBddNode node = new JBddInternalNode(var, low, high);
      newNodeCreated(node);
      return node;
    } else {
      JBddNode node = removeFirst();
      node.mutate(var, low, high);
      return node;
    } 
  }

  public void reportStatistics(PrintStream out) {
    out.println("  pre-allocated nodes : "+this.preAllocatedNodes);
    out.println("      allocated nodes : "+this.numberOfAllocations);
  }
}
